Nuprl Definition : rv-disjoint
11,40
postcript
pdf
rv-disjoint(
p
;
n
;
X
;
Y
)
==
i
:{0..
n
}.
==
(
s1
,
s2
:({0..
n
}
Outcome). (
j
:{0..
n
}. (
(
j
=
i
))
(
s1
(
j
) =
s2
(
j
)))
(
X
(
s1
) =
X
(
s2
)))
==
(
s1
,
s2
:({0..
n
}
Outcome).
==
(
j
:{0..
n
}. (
(
j
=
i
))
(
s1
(
j
) =
s2
(
j
)))
(
Y
(
s1
) =
Y
(
s2
)))
latex
clarification:
rv-disjoint(
p
;
n
;
X
;
Y
)
==
i
:{0..
n
}.
==
(
s1
:({0..
n
}
p-outcome(
p
)),
s2
:({0..
n
}
p-outcome(
p
)).
==
(
j
:{0..
n
}. (
(
j
=
i
))
(
s1
(
j
) =
s2
(
j
)
p-outcome(
p
)))
(
X
(
s1
) =
X
(
s2
)
))
==
(
s1
:({0..
n
}
p-outcome(
p
)),
s2
:({0..
n
}
p-outcome(
p
)).
==
(
j
:{0..
n
}. (
(
j
=
i
))
(
s1
(
j
) =
s2
(
j
)
p-outcome(
p
)))
(
Y
(
s1
) =
Y
(
s2
)
))
latex
Definitions
P
Q
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
{
i
..
j
}
,
#$n
,
P
Q
,
A
,
,
Outcome
,
s
=
t
,
,
f
(
a
)
FDL editor aliases
rv-disjoint
origin